(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const _30-0 (_ BitVec 30))
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(assert (or (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) v13 v13 (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) v13 v13 (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0)))
(assert (or (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) v13 v13 (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0))))
(assert (or (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0)))
(assert (or (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0))))
(assert (or (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) v13 (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0))))
(assert (or v13))
(assert (or (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0)))
(assert (or (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0))))
(assert (or (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) v4))
(assert (or (= (bvmul _30-0 (bvnand _30-0 _30-0)) _30-0) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) (= (bvnand _30-0 _30-0) (bvnand _30-0 _30-0)) v13))
(check-sat)
